Issue2763.agda:15,1-19
a != w of type A
when checking that the type ⊤ → (w : A) → G w b of the generated
with function is well-formed
